'Weak Dependency Graph [60.0]' ------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { a__c() -> a__f(g(c())) , a__f(g(X)) -> g(X) , mark(c()) -> a__c() , mark(f(X)) -> a__f(X) , mark(g(X)) -> g(X) , a__c() -> c() , a__f(X) -> f(X)} Details: We have computed the following set of weak (innermost) dependency pairs: { a__c^#() -> c_0(a__f^#(g(c()))) , a__f^#(g(X)) -> c_1() , mark^#(c()) -> c_2(a__c^#()) , mark^#(f(X)) -> c_3(a__f^#(X)) , mark^#(g(X)) -> c_4() , a__c^#() -> c_5() , a__f^#(X) -> c_6()} The usable rules are: {} The estimated dependency graph contains the following edges: {a__c^#() -> c_0(a__f^#(g(c())))} ==> {a__f^#(X) -> c_6()} {a__c^#() -> c_0(a__f^#(g(c())))} ==> {a__f^#(g(X)) -> c_1()} {mark^#(c()) -> c_2(a__c^#())} ==> {a__c^#() -> c_5()} {mark^#(c()) -> c_2(a__c^#())} ==> {a__c^#() -> c_0(a__f^#(g(c())))} {mark^#(f(X)) -> c_3(a__f^#(X))} ==> {a__f^#(X) -> c_6()} {mark^#(f(X)) -> c_3(a__f^#(X))} ==> {a__f^#(g(X)) -> c_1()} We consider the following path(s): 1) { mark^#(c()) -> c_2(a__c^#()) , a__c^#() -> c_0(a__f^#(g(c()))) , a__f^#(g(X)) -> c_1()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [0] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [0] x1 + [0] c_1() = [0] mark^#(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {a__f^#(g(X)) -> c_1()} Weak Rules: { a__c^#() -> c_0(a__f^#(g(c()))) , mark^#(c()) -> c_2(a__c^#())} Details: We apply the weight gap principle, strictly orienting the rules {a__f^#(g(X)) -> c_1()} and weakly orienting the rules { a__c^#() -> c_0(a__f^#(g(c()))) , mark^#(c()) -> c_2(a__c^#())} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {a__f^#(g(X)) -> c_1()} Details: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [1] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [1] c_0(x1) = [1] x1 + [0] a__f^#(x1) = [1] x1 + [1] c_1() = [0] mark^#(x1) = [1] x1 + [1] c_2(x1) = [1] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { a__f^#(g(X)) -> c_1() , a__c^#() -> c_0(a__f^#(g(c()))) , mark^#(c()) -> c_2(a__c^#())} Details: The given problem does not contain any strict rules 2) { mark^#(c()) -> c_2(a__c^#()) , a__c^#() -> c_0(a__f^#(g(c())))} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [0] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [0] x1 + [0] c_1() = [0] mark^#(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {a__c^#() -> c_0(a__f^#(g(c())))} Weak Rules: {mark^#(c()) -> c_2(a__c^#())} Details: We apply the weight gap principle, strictly orienting the rules {a__c^#() -> c_0(a__f^#(g(c())))} and weakly orienting the rules {mark^#(c()) -> c_2(a__c^#())} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {a__c^#() -> c_0(a__f^#(g(c())))} Details: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [1] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [8] c_0(x1) = [1] x1 + [1] a__f^#(x1) = [1] x1 + [0] c_1() = [0] mark^#(x1) = [1] x1 + [9] c_2(x1) = [1] x1 + [1] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { a__c^#() -> c_0(a__f^#(g(c()))) , mark^#(c()) -> c_2(a__c^#())} Details: The given problem does not contain any strict rules 3) { mark^#(c()) -> c_2(a__c^#()) , a__c^#() -> c_0(a__f^#(g(c()))) , a__f^#(X) -> c_6()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [0] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [0] x1 + [0] c_1() = [0] mark^#(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {a__f^#(X) -> c_6()} Weak Rules: { a__c^#() -> c_0(a__f^#(g(c()))) , mark^#(c()) -> c_2(a__c^#())} Details: We apply the weight gap principle, strictly orienting the rules {a__f^#(X) -> c_6()} and weakly orienting the rules { a__c^#() -> c_0(a__f^#(g(c()))) , mark^#(c()) -> c_2(a__c^#())} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {a__f^#(X) -> c_6()} Details: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [1] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [9] c_0(x1) = [1] x1 + [1] a__f^#(x1) = [1] x1 + [8] c_1() = [0] mark^#(x1) = [1] x1 + [9] c_2(x1) = [1] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { a__f^#(X) -> c_6() , a__c^#() -> c_0(a__f^#(g(c()))) , mark^#(c()) -> c_2(a__c^#())} Details: The given problem does not contain any strict rules 4) { mark^#(f(X)) -> c_3(a__f^#(X)) , a__f^#(g(X)) -> c_1()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [0] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [0] x1 + [0] c_1() = [0] mark^#(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {a__f^#(g(X)) -> c_1()} Weak Rules: {mark^#(f(X)) -> c_3(a__f^#(X))} Details: We apply the weight gap principle, strictly orienting the rules {a__f^#(g(X)) -> c_1()} and weakly orienting the rules {mark^#(f(X)) -> c_3(a__f^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {a__f^#(g(X)) -> c_1()} Details: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [1] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [1] x1 + [1] c_1() = [0] mark^#(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { a__f^#(g(X)) -> c_1() , mark^#(f(X)) -> c_3(a__f^#(X))} Details: The given problem does not contain any strict rules 5) { mark^#(c()) -> c_2(a__c^#()) , a__c^#() -> c_5()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [0] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [0] x1 + [0] c_1() = [0] mark^#(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {a__c^#() -> c_5()} Weak Rules: {mark^#(c()) -> c_2(a__c^#())} Details: We apply the weight gap principle, strictly orienting the rules {a__c^#() -> c_5()} and weakly orienting the rules {mark^#(c()) -> c_2(a__c^#())} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {a__c^#() -> c_5()} Details: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [0] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [1] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [0] x1 + [0] c_1() = [0] mark^#(x1) = [1] x1 + [1] c_2(x1) = [1] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { a__c^#() -> c_5() , mark^#(c()) -> c_2(a__c^#())} Details: The given problem does not contain any strict rules 6) {mark^#(c()) -> c_2(a__c^#())} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [0] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [0] x1 + [0] c_1() = [0] mark^#(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {mark^#(c()) -> c_2(a__c^#())} Weak Rules: {} Details: We apply the weight gap principle, strictly orienting the rules {mark^#(c()) -> c_2(a__c^#())} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {mark^#(c()) -> c_2(a__c^#())} Details: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [0] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [0] x1 + [0] c_1() = [0] mark^#(x1) = [1] x1 + [1] c_2(x1) = [1] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: {mark^#(c()) -> c_2(a__c^#())} Details: The given problem does not contain any strict rules 7) { mark^#(f(X)) -> c_3(a__f^#(X)) , a__f^#(X) -> c_6()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [0] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [0] x1 + [0] c_1() = [0] mark^#(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {a__f^#(X) -> c_6()} Weak Rules: {mark^#(f(X)) -> c_3(a__f^#(X))} Details: We apply the weight gap principle, strictly orienting the rules {a__f^#(X) -> c_6()} and weakly orienting the rules {mark^#(f(X)) -> c_3(a__f^#(X))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {a__f^#(X) -> c_6()} Details: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [0] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [1] x1 + [1] c_1() = [0] mark^#(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { a__f^#(X) -> c_6() , mark^#(f(X)) -> c_3(a__f^#(X))} Details: The given problem does not contain any strict rules 8) {mark^#(f(X)) -> c_3(a__f^#(X))} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [0] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [0] x1 + [0] c_1() = [0] mark^#(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {mark^#(f(X)) -> c_3(a__f^#(X))} Weak Rules: {} Details: We apply the weight gap principle, strictly orienting the rules {mark^#(f(X)) -> c_3(a__f^#(X))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {mark^#(f(X)) -> c_3(a__f^#(X))} Details: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [0] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [1] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [1] x1 + [0] c_1() = [0] mark^#(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: {mark^#(f(X)) -> c_3(a__f^#(X))} Details: The given problem does not contain any strict rules 9) {mark^#(g(X)) -> c_4()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [0] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [0] x1 + [0] c_1() = [0] mark^#(x1) = [0] x1 + [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {mark^#(g(X)) -> c_4()} Weak Rules: {} Details: We apply the weight gap principle, strictly orienting the rules {mark^#(g(X)) -> c_4()} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {mark^#(g(X)) -> c_4()} Details: Interpretation Functions: a__c() = [0] a__f(x1) = [0] x1 + [0] g(x1) = [1] x1 + [0] c() = [0] mark(x1) = [0] x1 + [0] f(x1) = [0] x1 + [0] a__c^#() = [0] c_0(x1) = [0] x1 + [0] a__f^#(x1) = [0] x1 + [0] c_1() = [0] mark^#(x1) = [1] x1 + [1] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] c_4() = [0] c_5() = [0] c_6() = [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: {mark^#(g(X)) -> c_4()} Details: The given problem does not contain any strict rules